//package test;
//
//import atom.UnaryAtom;
//import formula.BinaryFormula;
//import formula.Formula;
//import formula.TripleFormula;
//import formula.UnaryFormula;
//import literal.UnaryLiteral;
//import proof.ConclusionProof;
//import proof.Proof;
//import proof.ProofRule;
//import proof.RuleProof;
//import sign.FormulaSign;
//
//import java.util.ArrayList;
//
//public class TFnegatedTest {
//    public static void main(String[] args) {
//        UnaryFormula r = new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"), false));
//        UnaryFormula not_r = new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"), true));
//        UnaryFormula p1 = new UnaryFormula(new UnaryLiteral(new UnaryAtom("p1"), false));
//        //UnaryFormula p2 = new UnaryFormula(new UnaryLiteral(new UnaryAtom("p2"), false));
//        UnaryFormula pn = new UnaryFormula(new UnaryLiteral(new UnaryAtom("pn"), false));
//
//        BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,pn,r);
//        TripleFormula tf=new TripleFormula(FormulaSign.ANY,p1,bf);//ANY(p1,Exist(pn,r))
////        TripleFormula tf_negated=tf.getNegated();
////        System.out.println(tf);
////        System.out.println(tf_negated);
//
//        BinaryFormula bf2=new BinaryFormula(FormulaSign.ANY,pn,not_r);
//        TripleFormula tf2=new TripleFormula(FormulaSign.EXIST,p1,bf2);//Exist(p1,ANY(pn,not r))
//        System.out.println(tf2);
//        //System.out.println(tf2.isNegated(tf));
//
//        ArrayList<Proof> D3=new ArrayList<>();
//        Proof proof1=new ConclusionProof(tf);
//        Proof proof2=new ConclusionProof(tf2);
//        D3.add(proof1);
//        D3.add(proof2);
//        Proof proof=new RuleProof(D3, ProofRule.D3);
//        System.out.println(proof);
//
//
//
//    }
//
//}
